package list;

class Data {}

class SomeOne {
	public void work(/*@ readonly @*/ List l) {
		// The list is readonly, but we can create a local
		// iterator that we can modify via "next".
		
		/*@ peer @*/ ListIterRO itro = List.getIteratorRO(l);
		// in UTT:
		// peer ListIterRO itro = l.getIteratorRO_UTT();
		
		while( itro.hasCurrent() ) {
			System.out.println("Data: " + itro.getCurrent());
			itro.next();
		}
		
		/*@ readonly @*/ ListIterRW itrw = l.getIteratorRW();
		// itrw is readonly, therefore "next" and "remove" cannot be called
		// itrw.next();
	}
}

public class ListDemo {
	public void run() {
		List l = new /*@ rep @*/ List();
		l.add( new Data() );
		l.add( new Data() );
		
		// we have a RW reference to the list and
		// can therefore create a RW iterator.
		ListIterRW itrw = l.getIteratorRW();
		if( itrw.hasCurrent() ) {
			itrw.remove();
		}
		
		SomeOne so = new /*@ peer @*/ SomeOne();
		so.work( l );
		
		System.out.println("Done");
	}
	
	public static void main(String[] args) {
		new ListDemo().run();
	}
}
